\begin{tabbing}
pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\exists$$v$:$T$. $P$($x_{0}$,$v$)) $\Rightarrow$ ($\exists$$e$:E. loc($e$) $=$ $i$))\+
\\[0ex]\& vartype($i$;$x$) $\subseteq\rho$ $X$
\\[0ex]\& \=$\forall$$e$@$i$. kind($e$) $=$ locl($a$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$ \& $P$(($x$ when $e$),val($e$))\+
\\[0ex]\& $\forall$$e$@$i$. $\exists$$e$$\leq$${\it e'}$.kind(${\it e'}$) $=$ locl($a$) $\vee$ ($\forall$$v$:$T$. $\neg$$P$(($x$ after ${\it e'}$),$v$))
\-\\[0ex]\& @$i$ $x$ initially $x_{0}$:$X$
\-
\end{tabbing}